Termination proof of /tmp/tmppN2Jn_/LISTUTILITIES_nosorts

Termination of the following Term Rewriting System could be disproven:

Generalized rewrite system (where rules with free variables on rhs are allowed):
The TRS R consists of the following rules:

U11(tt) → U12(splitAt(N, XS))
U12(pair(YS, ZS)) → pair(cons(X), ZS)
and(tt) → X
tail(cons(N)) → XS
afterNth(N, XS) → snd(splitAt(N, XS))
fst(pair(X, Y)) → X
head(cons(N)) → N
natsFrom(N) → cons(N)
sel(N, XS) → head(afterNth(N, XS))
snd(pair(X, Y)) → Y
splitAt(0, XS) → pair(nil, XS)
splitAt(s(N), cons(X)) → U11(tt)
take(N, XS) → fst(splitAt(N, XS))

↳ GTRS

  ↳ CritRuleProof

Generalized rewrite system (where rules with free variables on rhs are allowed):
The TRS R consists of the following rules:

U11(tt) → U12(splitAt(N, XS))
U12(pair(YS, ZS)) → pair(cons(X), ZS)
and(tt) → X
tail(cons(N)) → XS
afterNth(N, XS) → snd(splitAt(N, XS))
fst(pair(X, Y)) → X
head(cons(N)) → N
natsFrom(N) → cons(N)
sel(N, XS) → head(afterNth(N, XS))
snd(pair(X, Y)) → Y
splitAt(0, XS) → pair(nil, XS)
splitAt(s(N), cons(X)) → U11(tt)
take(N, XS) → fst(splitAt(N, XS))

The rule U11(tt) → U12(splitAt(N, XS)) contains free variables in its right-hand side. Hence the TRS is not-terminating.